State principal types#91
Conversation
|
|
||
| .. note:: | ||
| For example, in isolation, the instruction :math:`\REFASNONNULL` has the type :math:`[(\REF~\NULL~\X{ht})] \to [(\REF~\X{ht})]` for any choice of valid :ref:`heap type <syntax-type>` :math:`\X{ht}`. | ||
| Moreover, if the input type :math:`[(\REF~\NULL~\X{ht})]` is already determined, i.e., a specific :math:`\X{ht}` is given, then the output type :math:`[(\REF~\X{ht})]` is fully determined as well. |
There was a problem hiding this comment.
Do we need to clarify somewhere that "input type" can mean both type parameters and input stack types?
There was a problem hiding this comment.
Input types only refers to stack operands here, i.e., the l.h.s. of an instruction type's arrow. Type immediates are always given, since they are a mandatory part of an instruction itself.
There was a problem hiding this comment.
Ah, I had previously misunderstood the example. Makes sense!
I do think this is worth stating as well. |
|
@tlively, done. Also added the symmetric statement about lubs, and a statement about the disjointness of subtyping hierarchies. PTAL. |
|
PS: I wonder if there is a concise mathematical term for a structure that's a (semi)lattice up to the lack of a top element (i.e., where elements can be unrelated), but I couldn't find anything. |
tlively
left a comment
tlively
left a comment
There was a problem hiding this comment.
Great! I'm happy to see conditional LUBs in there, since we heavily depend on their existence in Binaryen.
The trick of saying "this would be a lattice if you added this provisional top type" is what I would expect to see, FWIW. I don't know of a single term for that, either.
|
Do you think it would be worth presenting these properties briefly to the larger CG as an FYI since they in principle will constrain the design of other proposals as well? |
|
Yes, presenting them to the CG probably makes sense. I'll add an agenda item. |
|
@conrad-watt, please let me know if you still want to review this as well, otherwise I'll land it. |
Isn't this also the case for |
|
@askeksa-google, yes, you're right. I corrected the comment. |
|
@rossberg, multiple stakeholders on the V8 team still aren't sure the principle types property is worth the extra code size from annotations. Would you be able to connect us to a researcher (or anyone else) who has benefited or will benefit from this property? |
|
There is a meet-up of Wasm researchers next month, where I could try to gather some infos. That said, I don't think it's productive to ask for reopenening the debate. We made the decision, it took a long time to agree, there are other non-trivial issues that depend on the decision made, and most importantly, it is a conservative choice that could be amended later, which is not true the other way round. The usual criterion for revisiting a decision is significant new data. The only new discovery right now is the need for an additional annotation on two relatively cold and heavyweight instructions, which is likely in the noise. I don't think that justifies restarting the entire debate all over again, and after the prior resolution has already been implemented by everybody. We are on the final stretch of the MVP and I much rather focus on finishing up. |
That would be great, thanks! FWIW, we've measured these annotations to have a code size impact of a couple percentage points on top of the ~5% from the previous round of annotations, so the impact is small but not in the noise, and the cumulative impact of the annotations is moving out of "small" territory. This is a very real cost our users will be paying, so we'd just like to understand who benefits from it and how. |
|
I just measured with the latest sheets calc engine binary and the numbers are much better than the estimates I reported above:
Edit: I just discovered that the module does not actually contain any This points to missing optimization opportunities in Binaryen since it is not transforming any |
|
Thanks for the (updated) numbers! I take it then that you are fine with including the extra annotations on br_on_cast[_fail]? |
|
Corresponding numbers for a module produced by dart2wasm:
The code section (which is the only one affected by the annotations) is about 73% of the module size. As can be seen, the |
Yes, this PR LGTM. |
3 participants
As discussed in the last meeting, this describes the relevant Principal Types properties for Wasm, both informally and as a formal statement. It is written in the form of a small new section for the spec Appendix.
It states two forms of principality: the general property, assuming nothing about the type, and a non-standard partial "forward" property, assuming the input types are already known (as in an engine validator).
I checked all typing rules. Mostly these properties are straightforward to show, but there are two familiar friends causing extra complication for general principality:
br_table: Requires a glb over the types of the labels, which in turn requires proving that subtyping forms a semi-lattice. That is currently the case, but may be worth stating explicitly as well.selectwithout annotation: Requires introducing a special case type variable that only ranges over number and vector types.These properties also hold for the GC proposal, provided we go with source + target type annotation for
br_on_castandbr_on_cast_fail(ref.testandref.castonly need the target type, since they can be typed with the respective top type for input).@tlively, @conrad-watt, PTAL.